% easychair.tex,v 3.2 2012/05/15
%
% Select appropriate paper format in your document class as
% instructed by your conference organizers. Only withtimes
% and notimes can be used in proceedings created by EasyChair
%
% The available formats are 'letterpaper' and 'a4paper' with
% the former being the default if omitted as in the example
% below.
%
%\documentclass{easychair}
%\documentclass[debug]{easychair}
%\documentclass[verbose]{easychair}
%\documentclass[notimes]{easychair}
%\documentclass[withtimes]{easychair}
\documentclass[a4paper,withtimes]{easychair}
%\documentclass[letterpaper]{easychair}

% This provides the \BibTeX macro
\usepackage{doc}
\usepackage{macro}
%\usepackage{times}
\usepackage{enumerate,intestazione}
%\usepackage{makeidx}

% In order to save space or manage large tables or figures in a
% landcape-like text, you can use the rotating and pdflscape
% packages. Uncomment the desired from the below.
%
% \usepackage{rotating}
% \usepackage{pdflscape}

% If you plan on including some algorithm specification, we recommend
% the below package. Read more details on the custom options of the
% package documentation.
%
% \usepackage{algorithm2e}

% Some of our commands for this guide.
%
\newcommand{\easychair}{\textsf{easychair}}
\newcommand{\miktex}{MiK{\TeX}}
\newcommand{\texniccenter}{{\TeX}nicCenter}
\newcommand{\makefile}{\texttt{Makefile}}
\newcommand{\latexeditor}{LEd}

\newtheorem{theorem}{Theorem}%[section]
\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}

%\makeindex

%% Document
%%
\begin{document}

%% Front Matter
%%
% Regular title as in the article class.
%
\title{Session Types for Dynamically Evolvable \\ Communicating Systems}

% \titlerunning{} has to be set to either the main title or its shorter
% version for the running heads. When processed by
% EasyChair, this command is mandatory: a document without \titlerunning
% will be rejected by EasyChair

%\titlerunning{The {\easychair} Class File}

% Authors are joined by \and. Their affiliations are given by \inst, which indexes
% into the list defined using \institute
%
\author{
Cinzia Di Giusto\inst{1}
\and
Jorge A. P\'{e}rez\inst{2}
}

% Institutes for affiliations are also joined by \and,
\institute{
  CEA - LIST, France 
\and
   CITI and Department of Informatics, FCT - New University of Lisbon, Portugal 
 }
%  \authorrunning{} has to be set for the shorter version of the authors' names;
% otherwise a warning will be rendered in the running heads. When processed by
% EasyChair, this command is mandatory: a document without \authorrunning
% will be rejected by EasyChair

\authorrunning{Di Giusto and P\'{e}rez}


\clearpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\maketitle
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{abstract}
In recent work~\cite{dGP13}, we have 
developed a  session types discipline for a process calculus of \emph{adaptable processes}---a language for concurrency 
in which located processes may be stopped, duplicated, or even discarded along computation.
The intention is to understand whether known 
static analysis techniques for structured communications 
scale up to the challenging context of 
context-aware, adaptable distributed systems, in which 
disciplined communication %following precise protocols
and dynamic reconfiguration are intertwined concerns.
%collections of software artifacts which communicate following precise protocols and may dynamically evolve at runtime. 
Our work is an initial step towards this general goal; it is also 
driven by the observation that
type-based analyses of structured communications could be more effective/meaningful
if 
%the process languages on which they are typically grounded are
grounded on  process languages 
enhanced to represent central phenomena in emerging distributed systems.
We focus on dynamic reconfiguration, 
a crucial issue in, e.g., the
%third-party, 
cloud-based infrastructures 
in which distributed applications are deployed nowadays.
In this short paper, we informally present the framework in~\cite{dGP13}, illustrate it with examples, and 
discuss future developments.






\end{abstract}

%\setcounter{tocdepth}{2}
%{\small
%\tableofcontents}

%\section{To mention}
%
%Processing in EasyChair - number of pages.
%
%Examples of how EasyChair processes papers. Caveats (replacement of EC
%class, errors).

\pagestyle{empty}


%------------------------------------------------------------------------------
\section{Introduction}
\label{sect:introduction}

%The analysis of structured communications using 
The type-theoretic foundations 
%has been extremely fruitful.In particular, analysis techniques based on 
offered by \emph{session types} have proved successful
in the correctness analysis of complex communication scenarios. 
Numerous extensions of the original session types proposal 
have allowed 
to reason about 
advanced concepts and idioms in practical distributed programming.
Notably, this includes, e.g., forms of asynchronous~\cite{DBLP:conf/forte/KouzapasYH11} and  multiparty~\cite{DBLP:conf/popl/HondaYC08} communication. % have been integrated into session typed frameworks.
Interestingly, while many of such extensions appeal to sophistication in the 
type structure (by including, e.g., subtyping~\cite{DBLP:journals/acta/GayH05}, dependent/indexed types~\cite{DBLP:journals/corr/abs-1208-6483}, and kinding~\cite{DBLP:conf/concur/DemangeonH12}), the associated modeling language---the polyadic $\pi$-calculus---has remained essentially the same.
We thus observe an ``asymmetric'' progress between session types and process languages.
This should not appear as a surprise: because of its canonicity  and expressiveness,
the $\pi$-calculus turns out to be a rather natural and powerful choice for representing 
concurrent systems which interact by following precise--yet intricate---behavioral patterns.
%\todo{I would add the word powerful to underline the "expressiveness" of pi: i.e. to be a rather natural and powerful choice for representing  ... }

%In recent work, we have been investigating one such patterns, namely 
We are interested in one such patterns, namely \emph{dynamic reconfiguration}: it 
allows to represent the suspension, replacement, or abortion of running interacting processes. % at runtime.
As such, it can be useful to model and reason about important mechanisms in modern distributed systems, such as 
code mobility, online software update, failure recovery (as in, e.g., constructs for exceptions/compensations~\cite{DBLP:conf/concur/CarboneHY08,DBLP:books/sp/sensoria2011/FerreiraLRVZ11}), 
and scaling (the ability of acquiring/releasing computing resources at runtime, based on user demand).
These mechanisms typically have a global effect over the system and are meant to be performed atomically.
Hence, they appear 
%These features make dynamic reconfiguration 
difficult to implement as $\pi$-calculus specifications:
it is not obvious how name passing/scope extrusion---the central abstraction vehicles of the $\pi$-calculus---can 
be used to model 
this kind of global reconfiguration while retaining 
atomicity and a high-level of abstraction for reasoning. % purposes.

Based on these shortcomings of the $\pi$-calculus, 
and with the aim of setting a clean, formal framework for reasoning about communicating systems with dynamic reconfiguration, 
with Bravetti and Zavattaro we have developed
a framework of \emph{adaptable processes}~\cite{BGPZFMOODS}. Adaptable processes extend known %well-established 
process calculi with two constructs: located processes $l[P]$ and \emph{update processes} $l\{U\}$, where $U$ is a process context (a process with zero or more occurrences of a \emph{variable} $\mathsf{X}$). 
%\todo{see comment below also: i would say where $U$ is a process possibly containing some occurrences of  variable $\mathsf{X}$}.
While located processes aim at explicitly representing a distributed model
of interaction, update processes 
provide a built-in adaptation mechanism
%enforce the reconfiguration of 
for a portion of the model.
More precisely, by synchronizing on name $l$,
processes $l[P]$ and $l\{U\}$ 
may reduce to  
$U[P]$---the process resulting by 
%filling in the holes in $U$ with $P$.
substituting all occurrences of $\mathsf{X}$ with $P$.
%\todo{ there is a small issue here: in the sac paper and here we use variables, i am afraid it could be confusing to talk about holes, i suggest something like : $U[P]$---the process resulting by replacing variable $\mathsf{X}$ with $P$}
This way, we obtain a mechanism for process reconfiguration 
which is performed atomically in a single reduction.
%Key to this formal account of reconfiguration is then the shape of contexts $U$. 
%In~\cite{BGPZFMOODS} we have throughly studied this issue from the perspective of process verification.

%Sticking to the pi-calculus may be inconvenient in at least two cases:
%(i) when name-passing models turn out to be too level;
%(ii) when the behavioral patterns cannot be modeled in the pi-calculus.
%We are concerned with the latter issue.
%
%
%Nevertheless, 
%%given recent advances in the practice of distributed, concurrent programming 
%we argue wonder whether the point-to-point communication of the $\pi$-calculus 
%is a too low level foundation for describing structured communications. 
%%Indeed, distributed software applications are increasingly being deployed in 
%%open, context-aware settings in which novel behavioral patterns are available. 
%Notice that our question 
%goes beyond issues of language \emph{expressiveness} and concerns \emph{analysis convenience}  instead. 
%Take for instance, broadcast communication: even though broadcast communication 
%could be represented in the $\pi$-calculus, 
%the convenience of actually reasoning about a high-level behavioral pattern (broadcasting)
%in terms of low-level translations is questionable.
%%(Incidentally, we notice that the process language for multiparty sessions does include a form of broadcast.)
%
%The situation is more critical when point-to-point representations do not appear possible.
%This is the case of behavioral patterns for representing dynamic reconfiguration/adaptation.
%Indeed, the $\pi$-calculus fails to adequately capture process interactions in which whole process terms may appear and disappear:
%name reconfiguration (via scope extrusion) is a too low level mechanism. This expressiveness shortcoming was indeed
%part of our motivation for introducing a framework of \emph{adaptable processes}.
%By relying on a limited form of process-passing, adaptable processes may be stopped, replaced, or extended in a single reduction step.
%We conjecture that adaptable processes cannot be encoded in the $\pi$-calculus.

In recent work~\cite{dGP13}, we have started to explore
the integration of 
%:
a session-typed discipline
into a $\pi$-calculus with the two constructs above.
%dynamic reconfiguration/adaptation.
%adaptable processes. 
The intention is to understand whether 
%this well-established static analysis technique for structured communications
session types
scale up to the challenging context of 
context-aware, adaptable distributed systems, in which 
disciplined communication 
and dynamic reconfiguration are intertwined concerns.
Indeed, processes in our language
may evolve either by the usual forms of synchronization
but also by performing evolvability actions.
Hence, besides showing that well-typed processes respect session types along computation, 
we have proved that the interplay of communicating and evolvability actions is \emph{consistent}, i.e.,
an update action for a located process can only take place if such a process is not involved in 
already established sessions. That is, consistency ensures that 
evolvability steps do not interfere with the protocols 
enforced by session types.
From a technical perspective, our work
builds upon the approach of Garralda et al~\cite{DBLP:conf/ppdp/GarraldaCD06}
on session types for Ambients, 
and extends it to the case of adaptable processes 
which run in 
arbitrary, nested locations.

More broadly, our work is %an initial step towards this general goal; it is 
also 
driven by the observation that
type-based analyses of structured communications could be more effective/meaningful
if  grounded on  process languages 
enhanced to represent central phenomena in emerging distributed systems.
We have focused on dynamic reconfiguration; a similar observation may apply for other phenomena.
%We feel this is a promising (and rather unexplored) research strand.
%In this sense, our work may shed light on the foundations of modern programming languages.
In this short paper, we first summarize main elements of the framework of adaptable processes and
its integration with session types. Then we offer some examples, and conclude by discussing topics
for ongoing and future work.

%------------------------------------------------------------------------------
\section{A Framework of Disciplined,  Adaptable Processes}

%Rather than introducing our framework formally, in 
In this section we %this  presentation we %prefer to 
summarize the main elements of our approach. 
The interested reader is referred to~\cite{BGPZFMOODS} for further details and motivation for 
(untyped) adaptable processes, and to~\cite{dGP13} for  details on the 
notions given below, on the integration of binary session types and adaptable processes. 

\paragraph{Syntax and Semantics.}
We consider a minor extension of the usual polyadic $\pi$-calculus for binary session types (cf.~\cite{DBLP:conf/esop/HondaVK98}).
Besides the standard base sets for \emph{names} $a, b, x, \ldots$, \emph{channels} $c, d, \ldots$, \emph{labels} $n, n', \ldots$, 
and \emph{constants} $k, k', \ldots$, our process syntax relies on 
\emph{locations}, ranged over $l, l', \ldots$,
\emph{process variables}, ranged over $\mathsf{X}, \mathsf{X}', \ldots$;
\emph{recursion variables}, ranged over $Y, Y', \ldots$;
and \emph{integers}, ranged over $j,h,\ldots$. Our process language is thus given by the following grammar:
$$
\begin{array}{lrl}
\text{Expressions  }e	&::= & \!\!\! k  ~~\sepr ~~ e_1 + e_2 \sepr e_1 - e_2  \sepr \ldots \\
\text{Processes  }P \!\!& ::= &   \!\!\!\nopen{a}{c:\rho_\qua}.P  
	 ~~\sepr  ~~  \outC{c}{\tilde{e}}.P   	 ~~\sepr~~     \inC{c}{\tilde{x}}.P   	   	    ~~\sepr~~ P \parallel P 	 	     \\
&\sepr & 	  \!\!\!   \branch{c}{n_1:P_1, \ldots, n_k:P_k} ~~\sepr~~ \select{c}{n}.P 	 ~~\sepr~~   \throw{c}{d}.P     ~~\sepr~~    \catch{c}{d}.P   \\
 & \sepr & 	    \!\!\! \rec{Y{:}\Phi{\cdot}\Delta}{P}  ~~\sepr~ Y ~\sepr~~ \ifte{e}{P}{Q}~~\sepr~ \close{c}.P ~\sepr~\restr{u}{P}  
			    ~\sepr~\mathbf{0}
  \\
    & \sepr &   \!\!\!   \component{l}{h}{\Delta}{P} ~~(h \geq 0) ~~\sepr~~   \mathsf{X} ~~\sepr~~  \updated{l}{X}{\Delta_1}{\Delta_2}{P} 
  	    	    \end{array} 
$$
Processes in the first four lines are close to standard session-typed languages with session passing (delegation).
Differences are in the syntax for the session opening construct, and in the presence of an
explicit construct for session closing.
Following~\cite{DBLP:conf/ppdp/GarraldaCD06}, our language is instrumented with some elements which support the static analysis.
The type annotation for session establishment, denoted $\rho_\qua$, 
stands for a session type; its use
 is related to the fact that session types in a global computing scenario
represent decentralized service offerings. In the context of explicitly distributed processes, we consider this approach
(proposed by~\cite{DBLP:conf/ppdp/GarraldaCD06}) particularly sensible.
The closing construct is useful to count the number of active sessions in a given located process.
Novel constructs related to adaptable processes are in the last line.
We have located processes $\component{l}{h}{\Delta}{P}$ and update processes $\updated{l}{X}{\Delta_1}{\Delta_2}{P}$,
where 
$P(\mathsf{X})$ is a process with one or more occurrences of a variable $\mathsf{X}$.
Locations are transparent: hence,  in $\component{l}{h}{\Delta}{P}$ process $P$ may 
evolve autonomously until it is updated by an update action on $l$. %$\updated{l}{X}{\Delta_1}{\Delta_2}{Q}$.
One objective of our type system is then to discipline such update actions, so as to avoid updating processes which contain open sessions.
To this end, processes are  annotated:
while in $\component{l}{h}{\Delta}{P}$ we use $h$ to denote the number of \emph{active sessions} in $P$, 
in $\updated{l}{X}{\Delta_1}{\Delta_2}{P}$ both $\Delta_1$ and $\Delta_2$ denote type-based \emph{interfaces}---roughly, collections of 
session types.
A process $\updated{l}{X}{\Delta_1}{\Delta_2}{P}$ will be able to update a located 
process with interface (compatible with) $\Delta_1$ thus resulting in a (reconfigured) process with interface $\Delta_2$.
These annotations are central to the operational semantics, which is defined as a reduction relation.
We report some selected reduction rules below; we use contexts $C, D, E$ to capture the nested location structure for processes.
{\small
$$
\begin{array}{rl}
 \rulename{r:Open} & E\big[C[\nopen{a}{c:\rho_{\qua}}.P] \parallel D[\nopen{a}{d:\overline{\rho}_{\qua}}.Q]\big] \pired  
 \restr{c'}{\big(E^{+}_{}\big[{C^{+}_{}[P\sub{c'}{c}] \parallel D^{+}_{}[Q\sub{c'}{d}]}\big]\big)} 
 \vspace{1mm}
\\
\rulename{r:I/O} &
E\big[C[\outC{c}{\tilde{e}}.P] \parallel D[\inC{c}{\tilde{x}}.Q]\big] \pired  E\big[C[P\sub{\tilde{k}}{\tilde{x}}] \parallel D[Q]\big] \quad (\tilde{e} \downarrow \tilde{k}) \vspace{1mm}
\\
\rulename{r:Upd} &
E\big[C[\component{l}{0}{}{Q}] \parallel D[\updated{l}{X}{\Delta_1}{\Delta_2}{P}]\big]~~ 
(\text{with }\intf{Q} \compat\Delta_1)\pired  E_{}\big[C[P\sub{Q}{\mathsf{X}}] \parallel D[\nil]\big] \vspace{1mm}
\\
\rulename{r:Pass} &
E\big[C[\throw{c}{d}.P] \parallel D[\catch{c}{d}.Q]\big] \pired E\big[C[P] \parallel D[Q]\big] \vspace{1mm}
\\
\rulename{r:Close} & 
E\big[C[\close{c}.P] \parallel D[\close{c}.Q]\big] \pired  E^{-}\big[C^{-}[P] \parallel D^{-}[Q]\big] \vspace{1mm}
\\
 \rulename{r:Res} & 
\text{if } P \pired P' ~~\text{then} ~~ \restr{u}{P} \pired \restr{u}{P'} %\vspace{2mm} \\
\end{array}
$$  
}
Rules 
 \rulename{r:Open} and \rulename{r:Close} use two operations over contexts, denoted 
$C^{+}$ and $C^{-}$. They are used to propagate the information that a new session has been opened or closed;
both operations are defined inductively on the structure of nested, located processes.
Rule \rulename{r:Upd} captures the essence of our notion of consistency:
a located process $Q$ can be updated only if (i)~it contains no active sessions, and 
(ii)~its interface (denoted $\intf{Q}$ in the rule) is \emph{compatible} with the update process. 
This is denoted $\intf{Q} \compat\Delta_1$. 
For the sake of generality, this compatibility relation over interfaces is left unspecified.


\paragraph{Type System and Main Results.}
Our type syntax is given below.
We have deliberately aimed at retaining a type structure close to standard session types presentations.
$$
\begin{array}{lrl}
\text{Basic types  } \capab & ::= & \mathsf{int} \sepr \mathsf{b ool} \sepr \dots ~~~ \\
\text{Pre-session types  }\zeta & ::= & \epsilon  \!
		~~\sepr~~   !(\tilde{\capab}).\zeta 
		~~\sepr~~ ?(\tilde{\capab}).\zeta  
		~~\sepr~~   !(\sigma).\zeta 
		~~\sepr~~ ?(\sigma).\zeta 
		~~\sepr~~   t 
		~~\sepr~~   \mu t.\zeta \\
	& \sepr & 	  \&\{n_1:\zeta_1, \dots,  n_k:\zeta_k \}   
		~~\sepr~~   \oplus\{n_1:\zeta_1, \dots , n_k:\zeta_k \}   \\
\text{Closed pre-session types  } \rho & \triangleq &  \{ \zeta ~|~ \mathsf{ftv}(\zeta) = \emptyset\} \\
%\text{Type Qualifiers  } \qua & ::= & \qual \sepr \quau  \! \\
\text{Session types  }\omega &::=& \rho_\qua \sepr 	\bot 
\end{array}
$$
    
%    
%    \textsc{Environments}
%$$
%\begin{array}{lclr}
%\Delta &\!\!\!::= & \!\!\! \emptyset \sepr \Delta, \langle \rho, k \rangle & \text{process interface} \\
%\Phi & ::= & \!\!\! \emptyset \sepr \Phi, c:\omega & \text{active sessions}\\
%\Gamma &::= & \!\!\! \emptyset \sepr \Gamma, e:\capab & \text{first-order env.}\\
%\Theta &::= & \!\!\! \emptyset \sepr \Theta, Y:\Phi{\cdot}\Delta \sepr \Theta,\mathsf{X}:\Delta & \text{higher-order env.}
%\end{array}
%$$
Session types are annotated with a linear or unrestricted \emph{qualification}, denoted $\qua$; this is necessary to type
process recursion. To formalize typing environments, we consider interfaces $\Delta$, which are collections of 
closed pre-session types $\rho$. Intuitively, these represent available but not yet open sessions.
We also require a
set $\Phi$ which collects information on already active sessions: it records 
a channel name  and its associated session type. 
While $\Gamma$ is a first-order environment which maps expressions with basic types $\capab$,
the higher-order environment $\Theta$ stores the type of process/recursion variables.
This way, a \emph{type judgment} is  of form
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}} $$
stating that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\Phi$ and interface %(a collection of not yet open sessions) 
$\Delta$. We only present typing rules for adaptable and update processes; see~\cite{dGP13} for a full account.
$$
\begin{array}{lcclc}
\rulename{t:Loc} & \cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}} \qquad h = \#\{c \mid c:\omega \in \Phi\} }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\Delta}{P} }{ \type{\Phi}{\Delta}}} &    &
\rulename{t:Upd}   & 
\cfrac{\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\Delta_1}}}{P}{\type{\emptyset}{ \Delta_2 }}}{\judgebis{\env{\Gamma}{\Theta}}{\updated{l}{X}{\Delta_1}{\Delta_2}{P}}{\type{\emptyset}{ \emptyset}}}
\end{array}
$$
While rule $\rulename{t:Loc}$ checks that the annotation for located processes corresponds to the number of open sessions, 
rule $\rulename{t:Upd}$ ensures that the annotations for update processes correspond to the interface of the variable involved,
and to that offered by the process.

We close this section by summarizing the main properties of well-typed processes.
Process $P$ is said to be \emph{communicating} over channel $c$
if it sends (resp. receives) a value/session on $c$, if it makes a selection (resp. offers a choice), or if 
it closes a session on $c$. Then, 
two communicating processes are \emph{dual} on session $c$ if they are complementary to each other:
i.e., if one sends, the other receives on $c$; if one makes a selection, the other chooses; or if they are closing the same session $c$.
Let us write $Q_{\langle c \rangle}$ and $\overline{Q}_{\langle c \rangle}$ for two dual communicating processes on $c$.
Also, let $\pired_r$ stand for an update action, i.e., 
a reduction inferred using rule $\rulename{r:Upd}$ (possibly 
with the interplay of restriction/structural congruence rules).
We say that %\begin{definition}[Consistency]\label{d:consist}%
a session on channel $c$ is \emph{consistent} in a process $P$ if,
for all $P', P''$ such that 
$$P \pired^{*} P' \equiv (\nu \tilde{u})\big (E\big[C[Q_{\langle c \rangle}] \parallel D[\overline{Q}_{\langle c \rangle}]\big] \big)$$
%where $R$ and $Q$ are dual communicating processes in that session, 
and $P' \pired_r P''$, then $\exists E', C', D'$ such that
$P'' \equiv (\nu \tilde{u})\big (E'\big[C'[Q_{\langle c \rangle}] \parallel D'[\overline{Q}_{\langle c \rangle}]\big]\big)$.
%\end{definition}
Hence, intuitively, our notion of consistency formalizes the fact that
reductions corresponding to update actions do not disrupt the behavior of communicating processes
in already active sessions. They can only involve parts of the system not engaged into active sessions.
%\todo{Maybe this part above can be shortened, one could give just the intuition without giving the complete definition of consistency, it is quite complicate and does not add much to a quick understanding}


We have shown that all sessions in our well-typed processes are consistent. 
This result follows from the \emph{subject reduction} theorem below: i.e., well-typedness is preserved by reduction.

\begin{theorem}[Subject reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}}$ and $P \pired Q$ then one of the following holds: \\ %vspace{-2mm}
%\begin{enumerate}[(1)]
% \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta}}$;
% \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta\sub{v}{x}}}$;
%  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta'}}$ for some $\Delta'$
%  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi, c:\bot}{\Delta\ominus\{\rho, \overline{\rho}\}}}$ for some $\rho$;
 (1)~ $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta}}$; \qquad 
  (2)~$\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta'}}$, for some $\Delta'$; \\
  (3)~$\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi, c:\bot}{\Delta'}}$, for some $\Delta' \subset \Delta$ and channel $c$.
%\end{enumerate}
\end{theorem}

The above items correspond to  the different possibilities for reduction.
%Item~(1) is related to rules 
%\rulename{r:I/O}, \rulename{r:Pass},
%\rulename{r:Rec}, \rulename{r:IfTr}, \rulename{r:IfFa}, \rulename{r:Close}, \rulename{r:Res}, \rulename{r:Str}, and \rulename{r:Sel}. 
%Item~(2) captures the case of a reduction via rule \rulename{r:Upd}: the exact shape of 
%$\Delta'$ is obtained from $\Delta$ by considering the update process that has changed some located process 
%with interface $\Delta_1$ into a process with interface $\Delta_2$. 
%Item~(3) follows from \rulename{r:Open}.
The main consequence of 
Thm.~\ref{th:subred} is the \emph{absence of communication errors}
for well-typed processes. 
It also 
allows us to prove that every session that is established along the evolution of a process is \emph{consistent}.
We can indeed state:

\begin{corollary}[Con\-sist\-ency by Typing]\label{cor:cons}
Suppose  
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}} $
is a well-typed process.
Then every session $\rho_\qua \in \Delta$ %that can be established along the evolution of $P$, we have that 
is consistent. %, in the sense of Def.~\ref{d:consist}.
\end{corollary}

%Theorem~\ref{th:subred} allows us to prove that every session that is established along the evolution of a process is consistent, i.e., sessions inside  adaptable processes cannot be disrupted by an update. 
This result follows from Thm.~\ref{th:subred} 
by observing that 
enabling update actions only for 
located processes without active sessions (cf. rule \rulename{r:Upd}), essentially 
rules out the possibility of 
updating a location containing 
a communicating process $P_{\langle c \rangle}$, as defined above.
Indeed, our type system ensures that the annotations enabling update actions 
are correctly assigned and maintained along reduction.


%\section{Disciplined Adaptable Processes by Examples}
%We have argued that name passing as in the $\pi$-calculus may not always
%be enough to adequately capture scenarios of dynamic reconfiguration in session-typed scenarios.
%We illustrate this point by means of a simple example, 
%in which we combine \emph{delegation} (session passing)
%and reconfiguration via adaptable processes so as to obtain more expressive specifications.
%Let us 
%consider a simple scenario of distributed, interacting services (a client $C$ and a service $S$), conveniently represented as located processes:
%$$
%\mathsf{Sys} \triangleq \component{l_{1}}{0}{}{C} \parallel \bigcomponent{l_2}{0}{}{\component{r}{0}{}{S} \parallel R} \quad\text{where:}\vspace{-3mm}
%$$
%% We define $C$ and $S$ as follows:
%\begin{eqnarray*}
%C \!\!& \!\!\triangleq \!\!& \nopen{a}{c:\overline{\sigma}}.\outC{c}{u,p}.\branch{c}{n_1{:}Q_1 \parallel n_1{:}Q_2}.\close{c} \\
%S \!\!& \!\!\triangleq \!\!& \nopen{a}{s:\sigma}.\inC{s}{u,p}.\select{s}{n_1.P_1}.\close{s} 
%\end{eqnarray*}
%and where $R$ represents the platform in which $S$ is deployed.
%$\mathsf{Sys}$ may proceed by establishing a session of type $\sigma$ between $S$ and $C$
%(realized by $P_1$ and $Q_1$).
%Suppose that $R$ stands for an adaptation routine for $S$, defined as an update process:
%$$
%R \triangleq \mupdate{r}{\component{r_1}{0}{}{S'}  \parallel \component{r_2}{0}{}{T} }{\sigma}{\Delta} \quad\text{where:}\vspace{-3mm}
%$$
%\begin{eqnarray*}
%S' \!\!& \!\!\triangleq \!\!&\!\!\nopen{a}{s:\sigma}.\nopen{b}{d:!(\sigma)}.\throw{d}{s}.\close{d} \\
%T \!\!& \!\!\triangleq \!\!& \!\!\nopen{b}{e:?(\sigma)}.\catch{e}{s}.\inC{s}{u,p}.\select{s}{n_1.P_1}.\close{s}.\close{e} 
%\end{eqnarray*}
%%represents a simple adaptation routine enforcing explicit distribution of interacting processes.
%Because $R$ declares no process variables,
%it formalizes an update operation which \emph{discards} the behavior located at $r$. We have:
%\begin{equation}
%\mathsf{Sys} \pired \component{l_{1}}{0}{}{C} \parallel \bigcomponent{l_2}{0}{}{\component{r_1}{0}{}{S'}  \parallel \component{r_2}{0}{}{T}} \label{eq:ex}
%\end{equation}
%Thus, 
%an update action on $r$
%reconfigures the distributed structure of $S$:
%in a single step, 
%the monolithic service $S$ is replaced by a more flexible 
%implementation in which $S'$ (located at $r_1$) first establishes a session with $C$ and then \emph{delegates} it to $T$ (located at $r_2$).
%This update action is transparent to $C$; it 
%%Note that the above update % synchronization on $r$ 
%is possible because
%the interface of $S$ (i.e., $\sigma$)  coincides with the annotation of $R$.
%Also, observe that interface $\Delta$ contains entries for session types $!(\sigma)$ and $?(\sigma)$,
%which are declared in $S'$ and $T$, resp.
%
%As a simple example of a ``more conservative'' reconfiguration policy for the server $S$, consider the following alternative definition for 
%$R$:
%
%$$
%R \triangleq 
%\ifte{e}{\mupdate{r}{\component{r_3}{0}{}{\mathsf{X}}}{\sigma}{\Delta}}
%{\mupdate{r}{\component{r_1}{0}{}{S'}  \parallel \component{r_2}{0}{}{T} }{\sigma}{\Delta}}
%$$
%in which $S', T$ are as defined above. This new definition of $R$ simply captures how update actions
%can be used in combination with standard process constructs to define expressive reconfiguration policies.
%More precisely, $R$ above says that depending on the boolean value $e$ reduces to, we will
%either relocate the server, preserving its behavior but placing it in location $r_3$, i.e.:
%$$
%\mathsf{Sys} \pired^* \component{l_{1}}{0}{}{C} \parallel \bigcomponent{l_2}{0}{}{\component{r_3}{0}{}{S}} 
%$$
%or perform the delegation-based reconfiguration scheme, as
%in (\ref{eq:ex}) above.
%%It is not difficult to see that, in the first case, we have the following sequence of reductions:
%
%
%
%%This example can be easily extended with infinite behavior 
%%(e.g., with $S$ and $R$ as persistent services) 
%%and with multiple clients. % $C_1, \ldots, C_k$. 
%The above scenario  illustrates how
%our framework extends the expressiveness of session-typed languages
%with located and update processes. % and update actions.
%Our type system not only ensures correct communications between $C$ and $S$:
%by relying on Cor.~\ref{cor:cons}, we know that well-typedness also implies
%session consistency, i.e., % between $C$ and $S$, i.e., 
%an update action on  $r$ will not occur if $C$ and $S$ have already initiated a session.

%\todo{i do not understand very well the previous paragraph, i would remove "already"  from the first sentence and "not only" from the second}
%\subsection{More interesting server}
%
%
%We consider the interaction between a Client and a Server as the process $S \parallel C$. 
%The behavior of the server is encoded trough an adaptable process that recursively establishes new sessions with clients:
%$$ S ::= \component{s}{0}{\Delta}{\rec{X:\emptyset, \Delta}{(\open{c:\rho}.c(x).\close{c} \parallel X)} }$$ 
%where $\Delta= \emptyset \shortmid \{\rho\}$ and $\rho = ?(int).\epsilon$.
%
%Clients, in order to connect to the server, must implement a session that is the dual of the one described above: 
%$$C ::= \open{c:\overline{\rho}}.\outC{c}{e}.\close{c}$$
%where $e$ is an expression that evaluates to  $int$.
%
%We now extend this scenario introducing a way of updating the server: $S \parallel C \parallel U$. Here, the update $U$ is meant to extend  the capabilities (for instance by enhancing its performance) of the server by adding an auxiliary machine $M$. The server is then delegating its sessions to $M$:
%$$
%\begin{array}{ll}
%U ::= & \updated{s}{X}{\Delta}{\Delta}{(\component{s}{0}{\Delta}{\rec{X:\emptyset, \Delta}{(\open{c:\rho}.\\
%& \qquad \qquad \open{d:\sigma}.\throw{d}{c}.\close{d}} \parallel X)} \parallel M)}\\
%M ::= &\component{m}{0}{\Delta'}{\rec{X:\emptyset, \Delta'}{(\open{d:\overline{\sigma}}.\catch{d}{e}.\\
%&  \qquad \qquad e(x).\close{e}.\close{d} \parallel X)}}
%\end{array}
% $$
%where $\Delta' = \emptyset \shortmid \ \{\overline{\sigma}\}$ and $\sigma = !(\rho).\epsilon$.




%T = open 

\section{Example: Dynamic Update in Workflow Applications}

\input{cinziaexam}
\section{Future Work}

As we have explained above, the work reported in this short note is only 
an initial step towards the comprehensive integration
of issues of dynamic evolution in models of communicating systems
which interact following precise typing disciplines.
Thus, there are several open issues we intend to explore in future work.
Next, we elaborate on some of them. 

\begin{enumerate}[-]
\item We would like to establish stronger correctness properties
for adaptable, session-typed processes, in particular \emph{progress (deadlock freedom)}.
This includes adapting to our setting known type systems for ensuring progress in session types~\cite{DLYTGC07,DBLP:journals/corr/abs-1010-5566}, but also
understanding whether 
the information added by such systems (e.g., orderings on session events)
can be exploited by %combined with 
mechanisms
which, by relying on appropriate update actions,  
could prevent/overcome deadlocked sessions at runtime.

%\item Related to the above, here we have described a very simple way of resolving the interplay of communication and evolvability:
%communication actions 
%have priority over update steps.
%As such, the update of a located process is only executed when the sub-processes it contains do not have open sessions.
%This may be inconvenient when already established sessions need to be aborted (as in a session with infinite or deadlocked behavior).
%We would like to refine our current model  
%so as to capture more naturally this kind of scenarios, in which update steps need to be ``forced''.


\item We imagine that our current scheme of nested, transparent locations (including the treatment of the information on open sessions)
may be too ``open'' for some applications. In fact, we would like to have ways of enforcing 
\emph{secure updates}, so as to protect located processes from unintended evolvability actions---as in, for instance, 
update actions triggered by \emph{unauthorized} users, or update actions 
based on \emph{permissions} for replacing, extending, or destroying the behavior of a located process.
%which completely discard the current behavior without having appropriate permissions to do so.

\item Finally, as our intention was to explore evolvability issues in known session type structures, 
we have refrained from enriching the typing system with information related to updates.
We think such an extension would not be difficult, and could offer a way to better control update actions.  
This way, for instance, one could decree (and statically check) that 
update actions occur only in selected parts of a communication protocol.
%and statically check that candidate programs attempt update operations accordingly.


\end{enumerate}
%------------------------------------------------------------------------------

%\begin{enumerate}[-]
%\item progress
%\item we privilege communication over updates; a more flexible interplay between update and sessions
%\end{enumerate}




\bibliographystyle{abbrv}
\bibliography{referen}

\end{document}

% EOF
